A, B, C:MsgA. A || B  C || A  C || B  C || A  B 

latex

Definitions

MsgA, t  T, x:A. B(x), M1 || M2, M1  M2, P  Q, IdLnk, x.A(x), x. t(x), 2of(t), rcv(l,tg), Type, f  g, Void, 1of(t), Top, Valtype(da;k), f(a), nat-deq-aux, <a,b>, NatDeq, atom-deq-aux, AtomDeq, #$n, a<b, False, x:AB(x), A, AB, , {x:A| B(x) }, , Atom, prod-deq(A;B;a;b), proddeq(a;b), product-deq(A;B;a;b), IdLnkDeq, x:AB(x), sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b), f(x)?z, s = t, S  T, State(ds), type List, S  T, f(x), Prop, f || g, b, P & Q, left+right, P  Q, b, , a:A fp B(a), x  dom(f), P  Q, Unit, if b t else f fi, x:A. B(x), {T}, locl(a), M1 ||decl M2, mk-ma, KindDeq, Knd, IdDeq, Id

Lemmas

fpf-compatible-join, locl wf, fpf-compatible-triple, fpf-join-dom2, fpf-join-ap-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf, fpf-ap wf, product-deq wf, idlnk-deq wf, fpf-cap wf, ma-state wf, ma-valtype wf, ma-state-subtype, Id wf, id-deq wf, subtype-fpf-cap-top, top wf, pi1 wf, subtype-fpf-cap-void, fpf-join wf, Kind-deq wf, rcv wf, pi2 wf, IdLnk wf, Knd wf, ma-compatible wf, msga wf